COM: int 1 summary

COM: int 1 intro

COM: INT DEFS acom

STM: le wf

COM: ge gt wf com

STM: gt wf

STM: comb for gt wf

STM: ge wf

STM: comb for ge wf

STM: comb for le wf

ABS: i  j < k

ABS: i  j  k

ABS: 

STM: nat wf

STM: nat properties

ABS: 

STM: nat plus wf

STM: nat plus properties

ABS: 

STM: int nzero wf

STM: int nzero properties

ABS: {i...}

STM: int upper wf

STM: comb for int upper wf

STM: int upper properties

ABS: {...i}

STM: int lower wf

STM: int lower properties

ABS: {i..j}

STM: int seg wf

STM: comb for int seg wf

STM: int seg properties

STM: decidable equal int seg

ABS: {i...j}

STM: int iseg wf

STM: int iseg properties

STM: int lt to int upper

STM: int le to int upper

COM: INT INCLUSIONS tcom

STM: nat plus inc nat

STM: nat plus inc

STM: nat plus inc int nzero

COM: INDUCTION tcom

STM: nat ind a

STM: nat ind tp

STM: nat ind

STM: comp nat ind tp

STM: comp nat ind a

STM: nat well founded

COM: OLD INDUCTION

STM: complete nat ind

ABS: suptype(S; T)

STM: complete nat ind with y

COM: int 1 end